import proveit
from proveit import defaults, ExprTuple, ExprRange
from proveit import k, m, s, t, U
from proveit.numbers import (
Mult, Exp, zero, one, two, subtract, exp2pi_i)
from proveit.linear_algebra import MatrixExp, TensorProd
from proveit.physics.quantum import var_ket_u, varphi
from proveit.physics.quantum.circuits import (
QcircuitEquiv, phase_kickbacks_on_register)
from proveit.physics.quantum.QPE import (
_s, _t, _ket_u, _U, _phase, _s_in_nat_pos, _u_ket_register,
_normalized_ket_u, _unitary_U, _phase_in_interval, _eigen_uu,
QPE1_def, _psi_t_def, _psi_t_ket_is_normalized_vec)
theory = proveit.Theory() # the theorem's theory
%proving _psi_t_output
# don't combine factors of 2
Mult.change_simplification_directives(combine_all_exponents=False,
combine_numeric_rational_exponents=False)
_psi_t_def
_psi_t = _psi_t_def.instantiate()
_psi_t_ket_is_normalized_vec
_psi_t_ket_is_normalized_vec.instantiate()
QPE1_def
QPE1_inst = QPE1_def.instantiate({s:_s, U:_U})
phase_kickbacks_on_register
Uexponentials = ExprTuple(ExprRange(k, MatrixExp(_U, Exp(two, k)),
subtract(t, one), zero, order='decreasing'))
phases = ExprTuple(ExprRange(k, Mult(Exp(two, k), _phase),
subtract(t, one), zero, order='decreasing'))
kickbacks = phase_kickbacks_on_register.instantiate(
{m:_s, U:Uexponentials, var_ket_u:_ket_u, varphi:phases})
kickbacks_with_QPE1 = QPE1_inst.sub_left_side_into(
kickbacks.inner_expr().lhs.operand)
For psi_t_tensor_u_expansion to simplify properly, we need to specify this default vector-space field, but we should be able to automate this in the future:
from proveit.numbers import Complex
from proveit.linear_algebra import VecSpaces
VecSpaces.default_field = Complex
psi_t_tensor_u__expansion = _psi_t.substitution(TensorProd(_psi_t.lhs, _ket_u))
output_consolidation = kickbacks_with_QPE1.lhs.operand.output_consolidation(
replacements=[psi_t_tensor_u__expansion.derive_reversed()])
output_consolidation_from_desired = _psi_t_output.instance_expr.lhs.operand.output_consolidation()
equiv = output_consolidation.apply_transitivity(output_consolidation_from_desired)
equiv.sub_right_side_into(kickbacks_with_QPE1)
_psi_t_output may now be readily provable (assuming required theorems are usable). Simply execute "%qed".
%qed
proveit.physics.quantum.QPE._psi_t_output has been proven.
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | generalization | 1 | ⊢ | |
| 1 | instantiation | 4, 2, 3 | ||
| 2 | instantiation | 4, 5, 6 | ||
| 3 | instantiation | 7, 8, 9 | ||
| 4 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.rhs_prob_via_equiv | ||||
| 5 | instantiation | 10, 465, 753, 11, 12, 303, 13, 14, 15, 746, 748, 272, 16* | ||
| 6 | modus ponens | 17, 18 | ||
| 7 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.equiv_transitivity | ||||
| 8 | modus ponens | 19, 20 | ||
| 9 | instantiation | 31, 21 | ||
| 10 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.phase_kickbacks_on_register | ||||
| 11 | instantiation | 603, 22, 653, 360 | ||
| 12 | modus ponens | 23, 24 | ||
| 13 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._normalized_ket_u | ||||
| 14 | instantiation | 603, 25, 653, 360 | ||
| 15 | modus ponens | 26, 27 | ||
| 16 | instantiation | 690, 676, 738, 691, 28, 29, 692, 714, 695, 704, 705, 694 | ||
| 17 | instantiation | 47, 750, 471, 30 | ||
| 18 | instantiation | 31, 32 | ||
| 19 | instantiation | 47, 738, 750, 691, 48, 692 | ⊢ | |
| 20 | instantiation | 672, 33, 34 | ||
| 21 | modus ponens | 35, 36 | ||
| 22 | instantiation | 672, 37, 417 | ||
| 23 | instantiation | 419, 742, 743, 420 | ||
| 24 | generalization | 38 | ||
| 25 | instantiation | 672, 39, 417 | ||
| 26 | instantiation | 419, 742, 743, 420 | ||
| 27 | generalization | 40 | ||
| 28 | instantiation | 696 | ⊢ | |
| 29 | instantiation | 706 | ⊢ | |
| 30 | instantiation | 603, 41, 653, 360 | ||
| 31 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.equiv_reversal | ||||
| 32 | instantiation | 42, 465, 753, 59 | ||
| 33 | instantiation | 672, 43, 44 | ||
| 34 | instantiation | 238, 471, 67, 45, 46 | ||
| 35 | instantiation | 47, 738, 750, 691, 48, 692 | ⊢ | |
| 36 | instantiation | 82, 656, 49, 753, 465, 50, 51, 303, 52, 53, 54, 55, 56, 270, 543, 691, 471, 96, 57, 555* | ||
| 37 | instantiation | 466, 467 | ||
| 38 | instantiation | 58, 61, 358, 59 | ||
| 39 | instantiation | 466, 467 | ||
| 40 | instantiation | 60, 61, 707, 62 | ||
| 41 | instantiation | 672, 63, 417 | ||
| 42 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE.QPE1_def | ||||
| 43 | instantiation | 672, 64, 65 | ||
| 44 | instantiation | 238, 471, 66, 67, 68 | ||
| 45 | instantiation | 69, 471 | ||
| 46 | instantiation | 394, 745, 327, 328, 329, 330* | ||
| 47 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.circuit_equiv_temporal_sub | ||||
| 48 | instantiation | 706 | ⊢ | |
| 49 | instantiation | 706 | ⊢ | |
| 50 | instantiation | 706 | ⊢ | |
| 51 | instantiation | 70, 71 | ||
| 52 | instantiation | 603, 72, 73, 74 | ⊢ | |
| 53 | instantiation | 613, 75 | ⊢ | |
| 54 | instantiation | 706 | ⊢ | |
| 55 | instantiation | 613, 76 | ⊢ | |
| 56 | instantiation | 603, 77, 579, 78 | ⊢ | |
| 57 | instantiation | 181, 676, 79, 184, 80, 186 | ||
| 58 | conjecture | ⊢ | ||
| proveit.linear_algebra.matrices.exponentiation.U_closure | ||||
| 59 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._unitary_U | ||||
| 60 | conjecture | ⊢ | ||
| proveit.linear_algebra.matrices.exponentiation.unital2pi_eigen_exp_application | ||||
| 61 | instantiation | 414, 738, 81 | ||
| 62 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._eigen_uu | ||||
| 63 | instantiation | 466, 467 | ||
| 64 | instantiation | 82, 433, 83, 654, 84, 465, 85, 86, 87, 303, 88, 89, 90, 91, 92, 93, 94, 270, 169, 691, 95, 96, 97, 555, 98, 99*, 100*, 101* | ||
| 65 | instantiation | 238, 471, 102, 103, 104 | ||
| 66 | instantiation | 603, 105, 653, 360 | ||
| 67 | instantiation | 603, 106, 653, 360 | ||
| 68 | instantiation | 293, 294, 295, 443* | ||
| 69 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_from1_len_typical_eq | ||||
| 70 | theorem | ⊢ | ||
| proveit.logic.booleans.conjunction.left_from_and | ||||
| 71 | instantiation | 107, 753 | ||
| 72 | instantiation | 108 | ⊢ | |
| 73 | instantiation | 671 | ⊢ | |
| 74 | instantiation | 613, 109 | ⊢ | |
| 75 | instantiation | 214, 110, 555 | ⊢ | |
| 76 | instantiation | 268, 110, 543 | ⊢ | |
| 77 | instantiation | 111 | ⊢ | |
| 78 | instantiation | 613, 112 | ⊢ | |
| 79 | instantiation | 696 | ⊢ | |
| 80 | instantiation | 613, 445 | ||
| 81 | instantiation | 550, 113 | ||
| 82 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.output_consolidation | ||||
| 83 | instantiation | 603, 114, 130, 125 | ||
| 84 | instantiation | 357, 732, 743, 654, 289 | ||
| 85 | instantiation | 603, 115, 130, 125 | ||
| 86 | instantiation | 410, 116, 208 | ||
| 87 | modus ponens | 117, 118 | ||
| 88 | instantiation | 603, 119, 120, 121 | ||
| 89 | instantiation | 613, 122 | ||
| 90 | instantiation | 613, 123 | ||
| 91 | instantiation | 603, 124, 130, 125 | ||
| 92 | instantiation | 613, 126 | ||
| 93 | instantiation | 659, 127, 128 | ||
| 94 | instantiation | 603, 129, 130, 131 | ||
| 95 | modus ponens | 132, 133 | ||
| 96 | instantiation | 389, 471, 415 | ||
| 97 | instantiation | 134, 738, 385, 750, 135, 532, 136, 137 | ||
| 98 | instantiation | 659, 138, 139 | ||
| 99 | instantiation | 659, 140, 141 | ||
| 100 | instantiation | 659, 142, 143 | ⊢ | |
| 101 | instantiation | 659, 144, 145 | ||
| 102 | instantiation | 603, 146, 653, 360 | ||
| 103 | instantiation | 603, 147, 653, 360 | ||
| 104 | instantiation | 293, 294, 295 | ||
| 105 | instantiation | 350, 656, 148, 352, 353, 354, 385, 355* | ||
| 106 | instantiation | 672, 149, 417 | ||
| 107 | conjecture | ⊢ | ||
| proveit.physics.quantum.QPE._psi_t_ket_is_normalized_vec | ||||
| 108 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_3 | ||||
| 109 | instantiation | 672, 150, 151 | ⊢ | |
| 110 | instantiation | 389, 738, 380 | ⊢ | |
| 111 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_2 | ||||
| 112 | instantiation | 672, 152, 153 | ⊢ | |
| 113 | instantiation | 589, 737, 154 | ||
| 114 | instantiation | 350, 172, 155, 174, 175, 354, 385, 176* | ||
| 115 | instantiation | 350, 172, 156, 174, 175, 354, 385, 176* | ||
| 116 | instantiation | 410, 157, 158 | ||
| 117 | instantiation | 419, 732, 743, 289 | ||
| 118 | generalization | 159 | ||
| 119 | instantiation | 350, 172, 160, 161, 175, 354, 467, 162* | ||
| 120 | instantiation | 683, 714, 664 | ||
| 121 | instantiation | 613, 163 | ||
| 122 | instantiation | 214, 168, 555 | ||
| 123 | instantiation | 238, 471, 221, 164, 165 | ||
| 124 | instantiation | 350, 172, 166, 174, 175, 354, 385, 176* | ||
| 125 | instantiation | 613, 167 | ||
| 126 | instantiation | 268, 168, 169 | ||
| 127 | instantiation | 613, 170 | ||
| 128 | instantiation | 613, 171 | ||
| 129 | instantiation | 350, 172, 173, 174, 175, 354, 385, 176* | ||
| 130 | instantiation | 671 | ⊢ | |
| 131 | instantiation | 613, 177 | ||
| 132 | instantiation | 419, 742, 743, 420 | ||
| 133 | generalization | 178 | ||
| 134 | conjecture | ⊢ | ||
| proveit.logic.booleans.conjunction.disassociate | ||||
| 135 | instantiation | 706 | ⊢ | |
| 136 | instantiation | 603, 179, 486, 180 | ||
| 137 | instantiation | 181, 182, 183, 184, 517, 185, 186 | ||
| 138 | instantiation | 601, 187 | ||
| 139 | instantiation | 659, 188, 189 | ||
| 140 | instantiation | 601, 190 | ||
| 141 | instantiation | 613, 191 | ||
| 142 | instantiation | 601, 192 | ⊢ | |
| 143 | instantiation | 194, 654 | ⊢ | |
| 144 | instantiation | 601, 193 | ||
| 145 | instantiation | 194, 195 | ||
| 146 | instantiation | 350, 656, 196, 352, 353, 354, 385, 355* | ||
| 147 | instantiation | 672, 197, 417 | ||
| 148 | instantiation | 706 | ⊢ | |
| 149 | instantiation | 466, 467 | ||
| 150 | instantiation | 466, 198 | ⊢ | |
| 151 | instantiation | 659, 199, 200 | ⊢ | |
| 152 | instantiation | 466, 201 | ⊢ | |
| 153 | instantiation | 659, 202, 203 | ⊢ | |
| 154 | instantiation | 204, 742, 743, 740 | ||
| 155 | instantiation | 696 | ⊢ | |
| 156 | instantiation | 696 | ⊢ | |
| 157 | instantiation | 559, 560, 474, 205 | ||
| 158 | instantiation | 601, 206 | ||
| 159 | instantiation | 410, 207, 208 | ||
| 160 | instantiation | 696 | ⊢ | |
| 161 | instantiation | 696 | ⊢ | |
| 162 | instantiation | 659, 209, 210 | ||
| 163 | instantiation | 672, 211, 212 | ||
| 164 | instantiation | 603, 213, 653, 360 | ||
| 165 | instantiation | 214, 294, 401, 443* | ||
| 166 | instantiation | 696 | ⊢ | |
| 167 | instantiation | 470, 379 | ||
| 168 | instantiation | 446, 215, 216 | ||
| 169 | instantiation | 659, 217, 218 | ||
| 170 | instantiation | 238, 471, 222, 219, 220 | ||
| 171 | instantiation | 238, 471, 221, 222, 223 | ||
| 172 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.posnat3 | ||||
| 173 | instantiation | 696 | ⊢ | |
| 174 | instantiation | 696 | ⊢ | |
| 175 | instantiation | 696 | ⊢ | |
| 176 | instantiation | 659, 224, 225 | ||
| 177 | instantiation | 672, 226, 227 | ||
| 178 | instantiation | 446, 228, 229 | ||
| 179 | instantiation | 672, 230, 532 | ||
| 180 | instantiation | 613, 231 | ||
| 181 | conjecture | ⊢ | ||
| proveit.logic.booleans.conjunction.and_if_all | ||||
| 182 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.nat4 | ||||
| 183 | instantiation | 232 | ⊢ | |
| 184 | instantiation | 671 | ⊢ | |
| 185 | modus ponens | 233, 234 | ||
| 186 | instantiation | 671 | ⊢ | |
| 187 | instantiation | 607, 750, 691, 692, 237, 648, 664 | ||
| 188 | instantiation | 645, 691, 676, 750, 692, 235, 237, 664, 648, 684 | ||
| 189 | instantiation | 616, 738, 691, 236, 692, 237, 664, 684 | ||
| 190 | instantiation | 238, 471, 239, 301, 240 | ||
| 191 | instantiation | 601, 241, 242* | ||
| 192 | instantiation | 601, 555 | ⊢ | |
| 193 | instantiation | 601, 348 | ||
| 194 | conjecture | ⊢ | ||
| proveit.physics.quantum.circuits.unary_multi_output_reduction | ||||
| 195 | instantiation | 243, 244, 245 | ||
| 196 | instantiation | 706 | ⊢ | |
| 197 | instantiation | 466, 467 | ||
| 198 | instantiation | 507, 676, 246, 738, 380, 750 | ⊢ | |
| 199 | instantiation | 601, 485 | ⊢ | |
| 200 | instantiation | 639, 691, 738, 750, 692, 247, 714, 636, 684, 248* | ⊢ | |
| 201 | instantiation | 507, 676, 249, 750, 380 | ⊢ | |
| 202 | instantiation | 601, 485 | ⊢ | |
| 203 | instantiation | 639, 691, 738, 750, 692, 353, 684, 636, 250* | ⊢ | |
| 204 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.interval_upper_bound | ||||
| 205 | instantiation | 521, 560, 522, 251 | ||
| 206 | instantiation | 601, 252 | ||
| 207 | instantiation | 559, 560, 474, 253 | ||
| 208 | instantiation | 601, 254 | ⊢ | |
| 209 | instantiation | 459, 676, 255, 256, 462, 417 | ||
| 210 | instantiation | 659, 257, 258 | ||
| 211 | instantiation | 466, 259 | ||
| 212 | instantiation | 659, 260, 261 | ||
| 213 | instantiation | 350, 656, 262, 352, 353, 354, 385, 355* | ||
| 214 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.partition_front | ||||
| 215 | instantiation | 744, 263, 264 | ||
| 216 | instantiation | 498, 265 | ||
| 217 | instantiation | 645, 691, 738, 750, 692, 382, 664, 684, 648 | ||
| 218 | instantiation | 266, 684, 664, 619 | ||
| 219 | instantiation | 603, 267, 653, 360 | ||
| 220 | instantiation | 268, 269, 270, 271* | ||
| 221 | instantiation | 601, 272 | ||
| 222 | instantiation | 601, 273 | ||
| 223 | instantiation | 394, 712, 327, 274, 275, 276* | ||
| 224 | instantiation | 459, 676, 277, 278, 462, 532 | ||
| 225 | instantiation | 659, 279, 280 | ||
| 226 | instantiation | 466, 281 | ||
| 227 | instantiation | 659, 282, 283 | ||
| 228 | instantiation | 744, 737, 748 | ||
| 229 | instantiation | 622, 668, 544, 284, 285, 286*, 287* | ||
| 230 | instantiation | 466, 385 | ||
| 231 | instantiation | 470, 288 | ||
| 232 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_4_typical_eq | ||||
| 233 | instantiation | 419, 732, 743, 289 | ||
| 234 | generalization | 290 | ||
| 235 | instantiation | 696 | ⊢ | |
| 236 | instantiation | 706 | ⊢ | |
| 237 | instantiation | 751, 730, 291 | ||
| 238 | conjecture | ⊢ | ||
| proveit.core_expr_types.operations.operands_substitution_via_tuple | ||||
| 239 | instantiation | 603, 292, 653, 360 | ||
| 240 | instantiation | 293, 294, 295 | ||
| 241 | instantiation | 296, 753 | ||
| 242 | instantiation | 297, 691, 467, 750, 692, 417, 298, 299, 300, 301, 302, 303 | ||
| 243 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.pos_int_is_natural_pos | ||||
| 244 | instantiation | 744, 722, 748 | ||
| 245 | instantiation | 304, 477, 642, 305, 306, 307*, 308* | ||
| 246 | instantiation | 696 | ⊢ | |
| 247 | instantiation | 706 | ⊢ | |
| 248 | instantiation | 659, 309, 310 | ⊢ | |
| 249 | instantiation | 696 | ⊢ | |
| 250 | instantiation | 659, 311, 682 | ⊢ | |
| 251 | instantiation | 559, 560, 312, 562 | ||
| 252 | instantiation | 601, 313 | ||
| 253 | instantiation | 521, 560, 522, 314 | ||
| 254 | instantiation | 315, 714 | ⊢ | |
| 255 | instantiation | 696 | ⊢ | |
| 256 | instantiation | 696 | ⊢ | |
| 257 | instantiation | 607, 750, 691, 692, 684, 664 | ||
| 258 | instantiation | 639, 691, 738, 750, 692, 608, 684, 664, 682* | ||
| 259 | instantiation | 751, 513, 316 | ||
| 260 | instantiation | 601, 485 | ⊢ | |
| 261 | instantiation | 603, 317, 318, 319 | ||
| 262 | instantiation | 706 | ⊢ | |
| 263 | instantiation | 751, 752, 433 | ||
| 264 | instantiation | 698, 320, 435 | ⊢ | |
| 265 | instantiation | 574, 321 | ||
| 266 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_23 | ||||
| 267 | instantiation | 322, 323, 324* | ||
| 268 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.partition_back | ||||
| 269 | instantiation | 446, 325, 326 | ||
| 270 | instantiation | 583, 636, 684, 555 | ⊢ | |
| 271 | instantiation | 643, 684, 664, 619 | ||
| 272 | instantiation | 394, 745, 327, 328, 329, 330* | ||
| 273 | instantiation | 659, 331, 332 | ||
| 274 | instantiation | 613, 333 | ||
| 275 | instantiation | 613, 334 | ⊢ | |
| 276 | instantiation | 645, 691, 738, 750, 692, 335, 336, 648, 664 | ||
| 277 | instantiation | 696 | ⊢ | |
| 278 | instantiation | 696 | ⊢ | |
| 279 | instantiation | 645, 750, 738, 647, 684, 664, 648 | ||
| 280 | instantiation | 617, 691, 750, 692, 684, 664, 619 | ||
| 281 | instantiation | 507, 676, 337, 471, 380, 750 | ||
| 282 | instantiation | 601, 485 | ⊢ | |
| 283 | instantiation | 637, 750, 664, 684 | ||
| 284 | instantiation | 524, 731, 718 | ||
| 285 | instantiation | 338, 544, 731, 718, 339, 340 | ||
| 286 | instantiation | 603, 341, 342, 343 | ||
| 287 | instantiation | 603, 344, 345, 346 | ||
| 288 | instantiation | 446, 700, 347 | ||
| 289 | instantiation | 622, 544, 718, 680, 623, 440*, 473* | ||
| 290 | instantiation | 613, 348 | ||
| 291 | instantiation | 751, 733, 349 | ||
| 292 | instantiation | 350, 656, 351, 352, 353, 354, 385, 355* | ||
| 293 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.merge_front | ||||
| 294 | instantiation | 389, 691, 509 | ||
| 295 | instantiation | 613, 401 | ||
| 296 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._psi_t_def | ||||
| 297 | conjecture | ⊢ | ||
| proveit.linear_algebra.tensors.tensor_prod_disassociation | ||||
| 298 | instantiation | 603, 356, 653, 360 | ||
| 299 | instantiation | 357, 742, 743, 560, 420 | ||
| 300 | instantiation | 596, 358 | ⊢ | |
| 301 | instantiation | 603, 359, 653, 360 | ||
| 302 | modus ponens | 361, 362 | ||
| 303 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._u_ket_register | ||||
| 304 | conjecture | ⊢ | ||
| proveit.numbers.addition.strong_bound_via_left_term_bound | ||||
| 305 | instantiation | 751, 733, 363 | ||
| 306 | instantiation | 364, 642, 697, 723, 365, 366 | ||
| 307 | instantiation | 603, 367, 368, 369 | ||
| 308 | instantiation | 603, 370, 371, 372 | ||
| 309 | instantiation | 601, 373 | ⊢ | |
| 310 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.add_2_1 | ||||
| 311 | instantiation | 601, 374 | ⊢ | |
| 312 | instantiation | 713, 597, 375 | ||
| 313 | instantiation | 601, 376 | ||
| 314 | instantiation | 559, 560, 377, 562 | ||
| 315 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.complex_x_to_first_power_is_x | ||||
| 316 | instantiation | 492, 738, 691, 378, 692, 379, 380, 750, 493 | ||
| 317 | instantiation | 645, 691, 738, 692, 382, 381, 664, 684, 636 | ||
| 318 | instantiation | 637, 738, 750, 382, 664, 684 | ||
| 319 | instantiation | 639, 750, 738, 691, 608, 692, 664, 684, 682* | ||
| 320 | instantiation | 710, 383 | ⊢ | |
| 321 | instantiation | 610, 433 | ||
| 322 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.extended_range_len | ||||
| 323 | instantiation | 384, 385 | ||
| 324 | instantiation | 659, 386, 387 | ||
| 325 | instantiation | 744, 746, 497 | ||
| 326 | instantiation | 498, 388 | ||
| 327 | instantiation | 389, 390, 509 | ||
| 328 | instantiation | 613, 391 | ||
| 329 | instantiation | 613, 392 | ||
| 330 | instantiation | 659, 393, 588 | ||
| 331 | instantiation | 394, 742, 395, 396, 397 | ||
| 332 | modus ponens | 398, 399 | ||
| 333 | instantiation | 659, 400, 401 | ||
| 334 | instantiation | 659, 402, 555 | ⊢ | |
| 335 | instantiation | 706 | ⊢ | |
| 336 | instantiation | 751, 730, 403 | ||
| 337 | instantiation | 696 | ⊢ | |
| 338 | conjecture | ⊢ | ||
| proveit.numbers.ordering.less_eq_add_right | ||||
| 339 | instantiation | 423, 742, 743, 740 | ||
| 340 | instantiation | 404, 750 | ⊢ | |
| 341 | instantiation | 645, 691, 738, 750, 692, 591, 651, 684, 644 | ||
| 342 | instantiation | 645, 738, 691, 591, 647, 692, 651, 684, 664, 648 | ||
| 343 | instantiation | 659, 405, 425 | ||
| 344 | instantiation | 645, 691, 738, 750, 692, 406, 725, 684, 644 | ||
| 345 | instantiation | 645, 738, 691, 406, 647, 692, 725, 684, 664, 648 | ||
| 346 | instantiation | 617, 750, 691, 692, 725, 684, 664, 619 | ||
| 347 | instantiation | 498, 623 | ||
| 348 | instantiation | 659, 407, 408 | ||
| 349 | instantiation | 751, 736, 409 | ||
| 350 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.general_len | ||||
| 351 | instantiation | 706 | ⊢ | |
| 352 | instantiation | 706 | ⊢ | |
| 353 | instantiation | 706 | ⊢ | |
| 354 | instantiation | 410, 750, 462 | ⊢ | |
| 355 | instantiation | 659, 411, 412 | ||
| 356 | instantiation | 672, 413, 417 | ||
| 357 | conjecture | ⊢ | ||
| proveit.logic.booleans.conjunction.redundant_conjunction_general | ||||
| 358 | instantiation | 414, 738, 415 | ⊢ | |
| 359 | instantiation | 672, 416, 417 | ||
| 360 | instantiation | 613, 418 | ||
| 361 | instantiation | 419, 742, 743, 420 | ||
| 362 | generalization | 421 | ||
| 363 | instantiation | 751, 736, 422 | ||
| 364 | conjecture | ⊢ | ||
| proveit.numbers.ordering.less_eq_add_right_strong | ||||
| 365 | instantiation | 423, 732, 743, 728 | ||
| 366 | instantiation | 610, 656 | ⊢ | |
| 367 | instantiation | 645, 691, 738, 750, 692, 646, 651, 714, 426 | ||
| 368 | instantiation | 645, 738, 691, 646, 635, 692, 651, 714, 664, 685 | ||
| 369 | instantiation | 659, 424, 425 | ||
| 370 | instantiation | 645, 691, 738, 750, 692, 427, 679, 714, 426 | ||
| 371 | instantiation | 645, 738, 691, 427, 635, 692, 679, 714, 664, 685 | ||
| 372 | instantiation | 617, 750, 691, 692, 679, 714, 664, 579 | ||
| 373 | instantiation | 428, 714 | ⊢ | |
| 374 | instantiation | 428, 684 | ⊢ | |
| 375 | instantiation | 672, 429, 430 | ||
| 376 | instantiation | 601, 431 | ||
| 377 | instantiation | 713, 597, 432 | ||
| 378 | instantiation | 706 | ⊢ | |
| 379 | instantiation | 751, 513, 433 | ||
| 380 | instantiation | 698, 434, 435 | ⊢ | |
| 381 | instantiation | 706 | ⊢ | |
| 382 | instantiation | 706 | ⊢ | |
| 383 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.zero_set_within_int | ||||
| 384 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_len_is_nat | ||||
| 385 | instantiation | 672, 509, 436 | ||
| 386 | instantiation | 601, 602 | ||
| 387 | instantiation | 603, 437, 438, 439 | ||
| 388 | instantiation | 622, 544, 718, 680, 623, 440*, 516* | ||
| 389 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_nat_closure_bin | ||||
| 390 | instantiation | 751, 513, 441 | ⊢ | |
| 391 | instantiation | 659, 442, 443 | ||
| 392 | instantiation | 659, 444, 445 | ||
| 393 | instantiation | 645, 691, 738, 750, 692, 618, 621, 651, 664 | ||
| 394 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.shift_equivalence | ||||
| 395 | instantiation | 446, 447, 448 | ||
| 396 | instantiation | 613, 449 | ||
| 397 | instantiation | 613, 450 | ||
| 398 | instantiation | 451, 746, 748 | ||
| 399 | generalization | 452 | ||
| 400 | instantiation | 601, 455 | ⊢ | |
| 401 | instantiation | 659, 453, 454 | ||
| 402 | instantiation | 601, 455 | ⊢ | |
| 403 | instantiation | 751, 733, 456 | ||
| 404 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.natural_lower_bound | ||||
| 405 | instantiation | 617, 750, 691, 692, 651, 684, 664, 619 | ||
| 406 | instantiation | 706 | ⊢ | |
| 407 | instantiation | 645, 691, 676, 750, 692, 457, 679, 648, 664, 684 | ||
| 408 | instantiation | 616, 750, 691, 692, 679, 684, 664 | ||
| 409 | instantiation | 751, 727, 458 | ||
| 410 | theorem | ⊢ | ||
| proveit.logic.equality.sub_left_side_into | ||||
| 411 | instantiation | 459, 738, 460, 461, 462, 532 | ||
| 412 | instantiation | 659, 463, 464 | ||
| 413 | instantiation | 466, 467 | ||
| 414 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.exp_natpos_closure | ||||
| 415 | instantiation | 751, 513, 465 | ⊢ | |
| 416 | instantiation | 466, 467 | ||
| 417 | instantiation | 659, 468, 469 | ||
| 418 | instantiation | 470, 471 | ||
| 419 | conjecture | ⊢ | ||
| proveit.logic.booleans.conjunction.conjunction_from_quantification | ||||
| 420 | instantiation | 622, 544, 717, 680, 538, 472*, 473* | ||
| 421 | instantiation | 559, 560, 474, 475 | ||
| 422 | instantiation | 744, 722, 735 | ||
| 423 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.interval_lower_bound | ||||
| 424 | instantiation | 617, 750, 691, 692, 651, 714, 664, 579 | ||
| 425 | instantiation | 476, 664, 653 | ||
| 426 | instantiation | 751, 730, 477 | ||
| 427 | instantiation | 706 | ⊢ | |
| 428 | conjecture | ⊢ | ||
| proveit.numbers.addition.elim_zero_right | ||||
| 429 | instantiation | 703, 675, 478 | ||
| 430 | instantiation | 659, 479, 480 | ||
| 431 | instantiation | 601, 541 | ||
| 432 | instantiation | 672, 481, 482 | ||
| 433 | instantiation | 573, 753, 654 | ||
| 434 | instantiation | 710, 483 | ⊢ | |
| 435 | instantiation | 484, 485 | ⊢ | |
| 436 | instantiation | 603, 541, 486, 487 | ||
| 437 | instantiation | 645, 750, 738, 635, 636, 664, 685, 714 | ||
| 438 | instantiation | 637, 691, 676, 692, 488, 664, 685, 714 | ||
| 439 | instantiation | 620, 714, 664, 579 | ||
| 440 | instantiation | 603, 489, 490, 491 | ||
| 441 | instantiation | 492, 750, 691, 692, 493 | ⊢ | |
| 442 | instantiation | 601, 634 | ||
| 443 | instantiation | 659, 494, 495 | ||
| 444 | instantiation | 601, 634 | ||
| 445 | instantiation | 592, 664 | ||
| 446 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nonneg_int_is_natural | ||||
| 447 | instantiation | 744, 496, 497 | ||
| 448 | instantiation | 498, 499 | ||
| 449 | instantiation | 659, 500, 501 | ||
| 450 | instantiation | 583, 664, 502, 684, 516 | ||
| 451 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_fn_transformation | ||||
| 452 | instantiation | 659, 503, 504 | ||
| 453 | instantiation | 645, 691, 738, 750, 692, 591, 651, 684 | ||
| 454 | instantiation | 639, 750, 738, 691, 608, 692, 651, 684, 682* | ||
| 455 | instantiation | 663, 684 | ⊢ | |
| 456 | instantiation | 751, 736, 505 | ||
| 457 | instantiation | 696 | ⊢ | |
| 458 | assumption | |||
| 459 | axiom | ⊢ | ||
| proveit.core_expr_types.operations.operands_substitution | ||||
| 460 | instantiation | 706 | ⊢ | |
| 461 | instantiation | 706 | ⊢ | |
| 462 | instantiation | 643, 684, 619 | ⊢ | |
| 463 | instantiation | 645, 750, 738, 691, 647, 692, 684, 664, 648 | ||
| 464 | instantiation | 506, 684, 664, 619 | ||
| 465 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._s_in_nat_pos | ||||
| 466 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_len | ||||
| 467 | instantiation | 507, 676, 508, 691, 509, 750 | ||
| 468 | instantiation | 601, 541 | ||
| 469 | instantiation | 603, 510, 511, 512 | ||
| 470 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.range_from1_len | ||||
| 471 | instantiation | 751, 513, 753 | ||
| 472 | instantiation | 659, 514, 515 | ||
| 473 | instantiation | 603, 516, 619, 517 | ||
| 474 | instantiation | 518, 684, 519, 520 | ⊢ | |
| 475 | instantiation | 521, 560, 522, 523 | ||
| 476 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_reverse | ||||
| 477 | instantiation | 524, 680, 525 | ||
| 478 | instantiation | 672, 526, 527 | ||
| 479 | instantiation | 690, 750, 676, 691, 528, 692, 675, 704, 599, 694 | ||
| 480 | instantiation | 690, 691, 738, 676, 692, 677, 528, 714, 695, 704, 599, 694 | ||
| 481 | instantiation | 703, 675, 529 | ||
| 482 | instantiation | 659, 530, 531 | ||
| 483 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.zero_set_within_nat | ||||
| 484 | conjecture | ⊢ | ||
| proveit.logic.sets.enumeration.fold_singleton | ||||
| 485 | conjecture | ⊢ | ||
| proveit.numbers.negation.negated_zero | ||||
| 486 | instantiation | 671 | ⊢ | |
| 487 | instantiation | 613, 532 | ||
| 488 | instantiation | 696 | ⊢ | |
| 489 | instantiation | 659, 533, 534 | ||
| 490 | instantiation | 583, 609, 664, 714, 535 | ||
| 491 | instantiation | 671 | ⊢ | |
| 492 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_nat_pos_from_nonneg | ||||
| 493 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.less_0_1 | ||||
| 494 | instantiation | 645, 691, 738, 750, 692, 591, 651, 684, 664 | ||
| 495 | instantiation | 536, 664, 684, 653 | ||
| 496 | instantiation | 751, 752, 537 | ⊢ | |
| 497 | instantiation | 747, 732 | ||
| 498 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.nonneg_difference | ||||
| 499 | instantiation | 622, 642, 717, 680, 538, 539*, 540* | ||
| 500 | instantiation | 601, 541 | ||
| 501 | instantiation | 659, 542, 543 | ||
| 502 | instantiation | 751, 730, 544 | ||
| 503 | instantiation | 601, 545 | ||
| 504 | instantiation | 659, 546, 547 | ||
| 505 | instantiation | 751, 548, 549 | ||
| 506 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_13 | ||||
| 507 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_nat_closure | ||||
| 508 | instantiation | 696 | ⊢ | |
| 509 | instantiation | 550, 551 | ||
| 510 | instantiation | 645, 750, 738, 647, 636, 664, 648, 684 | ||
| 511 | instantiation | 637, 691, 676, 692, 552, 664, 648, 684 | ||
| 512 | instantiation | 620, 684, 664, 619 | ||
| 513 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat | ||||
| 514 | instantiation | 645, 750, 738, 691, 591, 692, 636, 651, 684 | ||
| 515 | instantiation | 637, 691, 738, 692, 591, 651, 684 | ||
| 516 | instantiation | 659, 553, 554 | ||
| 517 | instantiation | 613, 555 | ⊢ | |
| 518 | conjecture | ⊢ | ||
| proveit.numbers.division.div_complex_closure | ||||
| 519 | instantiation | 556, 714 | ⊢ | |
| 520 | instantiation | 557, 595, 558 | ⊢ | |
| 521 | conjecture | ⊢ | ||
| proveit.linear_algebra.addition.binary_closure | ||||
| 522 | conjecture | ⊢ | ||
| proveit.physics.quantum.algebra.ket_zero_in_qubit_space | ||||
| 523 | instantiation | 559, 560, 561, 562 | ||
| 524 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_real_closure_bin | ||||
| 525 | instantiation | 563, 723 | ⊢ | |
| 526 | instantiation | 703, 564, 694 | ||
| 527 | instantiation | 690, 691, 738, 750, 692, 565, 704, 599, 694 | ||
| 528 | instantiation | 696 | ⊢ | |
| 529 | instantiation | 672, 566, 567 | ||
| 530 | instantiation | 690, 750, 676, 691, 678, 692, 675, 704, 632, 694 | ||
| 531 | instantiation | 690, 691, 738, 676, 692, 677, 678, 714, 695, 704, 632, 694 | ||
| 532 | instantiation | 659, 568, 569 | ||
| 533 | instantiation | 645, 750, 738, 691, 591, 692, 684, 651 | ||
| 534 | instantiation | 659, 570, 571 | ||
| 535 | instantiation | 672, 578, 572 | ||
| 536 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_31 | ||||
| 537 | instantiation | 573, 654 | ⊢ | |
| 538 | instantiation | 574, 575 | ||
| 539 | instantiation | 659, 576, 577 | ||
| 540 | instantiation | 603, 578, 579, 580 | ||
| 541 | instantiation | 633, 651, 684, 634* | ||
| 542 | instantiation | 659, 581, 582 | ||
| 543 | instantiation | 583, 684, 714, 682 | ⊢ | |
| 544 | instantiation | 751, 733, 584 | ||
| 545 | instantiation | 645, 750, 738, 691, 591, 692, 621, 651, 684 | ||
| 546 | instantiation | 645, 691, 676, 738, 692, 585, 586, 621, 651, 684, 648, 664 | ||
| 547 | instantiation | 659, 587, 588 | ||
| 548 | instantiation | 741, 732, 746 | ||
| 549 | assumption | |||
| 550 | conjecture | ⊢ | ||
| proveit.numbers.negation.nat_closure | ||||
| 551 | instantiation | 589, 742, 590 | ||
| 552 | instantiation | 696 | ⊢ | |
| 553 | instantiation | 645, 750, 738, 691, 591, 692, 664, 651, 684 | ||
| 554 | instantiation | 643, 664, 684, 653 | ||
| 555 | instantiation | 592, 684 | ⊢ | |
| 556 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.sqrt_complex_closure | ||||
| 557 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.exp_rational_non_zero__not_zero | ||||
| 558 | instantiation | 593, 594, 595 | ⊢ | |
| 559 | conjecture | ⊢ | ||
| proveit.linear_algebra.scalar_multiplication.scalar_mult_closure | ||||
| 560 | instantiation | 596, 656 | ⊢ | |
| 561 | instantiation | 713, 597, 598 | ||
| 562 | conjecture | ⊢ | ||
| proveit.physics.quantum.algebra.ket_one_in_qubit_space | ||||
| 563 | conjecture | ⊢ | ||
| proveit.numbers.negation.real_closure | ||||
| 564 | instantiation | 703, 704, 599 | ||
| 565 | instantiation | 706 | ⊢ | |
| 566 | instantiation | 703, 600, 694 | ||
| 567 | instantiation | 690, 691, 738, 750, 692, 693, 704, 632, 694 | ||
| 568 | instantiation | 601, 602 | ||
| 569 | instantiation | 603, 604, 605, 606 | ||
| 570 | instantiation | 607, 750, 691, 692, 684, 651 | ||
| 571 | instantiation | 639, 691, 738, 750, 692, 608, 684, 651, 682* | ||
| 572 | instantiation | 683, 664, 609 | ||
| 573 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_nat_pos_closure_bin | ||||
| 574 | conjecture | ⊢ | ||
| proveit.numbers.ordering.relax_less | ||||
| 575 | instantiation | 610, 753 | ||
| 576 | instantiation | 645, 750, 738, 691, 646, 692, 636, 651, 714 | ||
| 577 | instantiation | 637, 691, 738, 692, 646, 651, 714 | ||
| 578 | instantiation | 659, 611, 612 | ||
| 579 | instantiation | 671 | ⊢ | |
| 580 | instantiation | 613, 682 | ⊢ | |
| 581 | instantiation | 659, 614, 615 | ||
| 582 | instantiation | 616, 691, 750, 692, 664, 714, 648 | ||
| 583 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.subtract_from_add | ||||
| 584 | instantiation | 751, 736, 742 | ||
| 585 | instantiation | 696 | ⊢ | |
| 586 | instantiation | 706 | ⊢ | |
| 587 | instantiation | 617, 738, 691, 750, 618, 692, 621, 651, 684, 664, 619 | ||
| 588 | instantiation | 620, 664, 621, 653 | ||
| 589 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nonpos_int_is_int_nonpos | ||||
| 590 | instantiation | 622, 670, 718, 680, 623, 624*, 625* | ||
| 591 | instantiation | 706 | ⊢ | |
| 592 | conjecture | ⊢ | ||
| proveit.numbers.addition.elim_zero_left | ||||
| 593 | conjecture | ⊢ | ||
| proveit.numbers.division.div_rational_nonzero_closure | ||||
| 594 | instantiation | 751, 627, 626 | ⊢ | |
| 595 | instantiation | 751, 627, 628 | ⊢ | |
| 596 | conjecture | ⊢ | ||
| proveit.linear_algebra.complex_vec_set_is_vec_space | ||||
| 597 | instantiation | 751, 730, 629 | ⊢ | |
| 598 | instantiation | 672, 630, 631 | ||
| 599 | instantiation | 713, 714, 644 | ||
| 600 | instantiation | 703, 704, 632 | ||
| 601 | axiom | ⊢ | ||
| proveit.logic.equality.substitution | ||||
| 602 | instantiation | 633, 651, 714, 634* | ||
| 603 | conjecture | ⊢ | ||
| proveit.logic.equality.four_chain_transitivity | ||||
| 604 | instantiation | 645, 750, 738, 635, 636, 664, 685, 684 | ||
| 605 | instantiation | 637, 691, 676, 692, 638, 664, 685, 684 | ||
| 606 | instantiation | 639, 750, 738, 691, 640, 692, 664, 685, 684, 641* | ||
| 607 | conjecture | ⊢ | ||
| proveit.numbers.addition.leftward_commutation | ||||
| 608 | instantiation | 706 | ⊢ | |
| 609 | instantiation | 751, 730, 642 | ||
| 610 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos | ||||
| 611 | instantiation | 645, 750, 738, 691, 646, 692, 664, 651, 714 | ||
| 612 | instantiation | 643, 664, 714, 653 | ||
| 613 | theorem | ⊢ | ||
| proveit.logic.equality.equals_reversal | ||||
| 614 | instantiation | 645, 691, 738, 750, 692, 646, 651, 714, 644 | ||
| 615 | instantiation | 645, 738, 691, 646, 647, 692, 651, 714, 664, 648 | ||
| 616 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_general_rev | ||||
| 617 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_general | ||||
| 618 | instantiation | 706 | ⊢ | |
| 619 | instantiation | 671 | ⊢ | |
| 620 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_32 | ||||
| 621 | instantiation | 751, 730, 649 | ||
| 622 | conjecture | ⊢ | ||
| proveit.numbers.addition.weak_bound_via_left_term_bound | ||||
| 623 | instantiation | 650, 753 | ||
| 624 | instantiation | 683, 684, 651 | ||
| 625 | instantiation | 652, 664, 653 | ||
| 626 | instantiation | 751, 655, 654 | ⊢ | |
| 627 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero | ||||
| 628 | instantiation | 751, 655, 656 | ⊢ | |
| 629 | instantiation | 751, 720, 657 | ⊢ | |
| 630 | instantiation | 703, 675, 658 | ||
| 631 | instantiation | 659, 660, 661 | ||
| 632 | instantiation | 713, 714, 662 | ||
| 633 | conjecture | ⊢ | ||
| proveit.numbers.negation.distribute_neg_through_binary_sum | ||||
| 634 | instantiation | 663, 664 | ||
| 635 | instantiation | 706 | ⊢ | |
| 636 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.complex_numbers.zero_is_complex | ||||
| 637 | conjecture | ⊢ | ||
| proveit.numbers.addition.elim_zero_any | ||||
| 638 | instantiation | 696 | ⊢ | |
| 639 | conjecture | ⊢ | ||
| proveit.numbers.addition.association | ||||
| 640 | instantiation | 706 | ⊢ | |
| 641 | instantiation | 672, 665, 666 | ⊢ | |
| 642 | instantiation | 751, 733, 667 | ||
| 643 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_triple_12 | ||||
| 644 | instantiation | 751, 730, 668 | ||
| 645 | conjecture | ⊢ | ||
| proveit.numbers.addition.disassociation | ||||
| 646 | instantiation | 706 | ⊢ | |
| 647 | instantiation | 706 | ⊢ | |
| 648 | instantiation | 724, 684 | ⊢ | |
| 649 | instantiation | 751, 733, 669 | ||
| 650 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound | ||||
| 651 | instantiation | 751, 730, 670 | ||
| 652 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.add_cancel_basic | ||||
| 653 | instantiation | 671 | ⊢ | |
| 654 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.posnat1 | ||||
| 655 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int | ||||
| 656 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.posnat2 | ||||
| 657 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.e_is_real_pos | ||||
| 658 | instantiation | 672, 673, 674 | ||
| 659 | axiom | ⊢ | ||
| proveit.logic.equality.equals_transitivity | ||||
| 660 | instantiation | 690, 750, 676, 691, 678, 692, 675, 704, 705, 694 | ||
| 661 | instantiation | 690, 691, 738, 676, 692, 677, 678, 714, 695, 704, 705, 694 | ||
| 662 | instantiation | 724, 679 | ||
| 663 | conjecture | ⊢ | ||
| proveit.numbers.negation.double_negation | ||||
| 664 | instantiation | 751, 730, 680 | ||
| 665 | instantiation | 681, 684, 714, 682 | ⊢ | |
| 666 | instantiation | 683, 684, 685 | ⊢ | |
| 667 | instantiation | 751, 736, 732 | ||
| 668 | instantiation | 751, 733, 686 | ||
| 669 | instantiation | 751, 736, 687 | ||
| 670 | instantiation | 751, 733, 688 | ||
| 671 | axiom | ⊢ | ||
| proveit.logic.equality.equals_reflexivity | ||||
| 672 | theorem | ⊢ | ||
| proveit.logic.equality.sub_right_side_into | ||||
| 673 | instantiation | 703, 689, 694 | ||
| 674 | instantiation | 690, 691, 738, 750, 692, 693, 704, 705, 694 | ||
| 675 | instantiation | 703, 714, 695 | ⊢ | |
| 676 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.nat3 | ||||
| 677 | instantiation | 706 | ⊢ | |
| 678 | instantiation | 696 | ⊢ | |
| 679 | instantiation | 751, 730, 697 | ||
| 680 | instantiation | 698, 699, 753 | ||
| 681 | conjecture | ⊢ | ||
| proveit.numbers.addition.subtraction.subtract_from_add_reversed | ||||
| 682 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.add_1_1 | ||||
| 683 | conjecture | ⊢ | ||
| proveit.numbers.addition.commutation | ||||
| 684 | instantiation | 751, 730, 718 | ⊢ | |
| 685 | instantiation | 724, 714 | ⊢ | |
| 686 | instantiation | 751, 736, 700 | ||
| 687 | instantiation | 751, 701, 702 | ||
| 688 | instantiation | 751, 736, 745 | ||
| 689 | instantiation | 703, 704, 705 | ||
| 690 | conjecture | ⊢ | ||
| proveit.numbers.multiplication.disassociation | ||||
| 691 | axiom | ⊢ | ||
| proveit.numbers.number_sets.natural_numbers.zero_in_nats | ||||
| 692 | conjecture | ⊢ | ||
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq | ||||
| 693 | instantiation | 706 | ⊢ | |
| 694 | instantiation | 751, 730, 707 | ⊢ | |
| 695 | instantiation | 751, 730, 708 | ⊢ | |
| 696 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_3_typical_eq | ||||
| 697 | instantiation | 751, 733, 709 | ||
| 698 | theorem | ⊢ | ||
| proveit.logic.sets.inclusion.unfold_subset_eq | ||||
| 699 | instantiation | 710, 711 | ⊢ | |
| 700 | instantiation | 744, 748, 712 | ||
| 701 | instantiation | 741, 746, 748 | ||
| 702 | assumption | |||
| 703 | conjecture | ⊢ | ||
| proveit.numbers.multiplication.mult_complex_closure_bin | ||||
| 704 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.complex_numbers.i_is_complex | ||||
| 705 | instantiation | 713, 714, 715 | ||
| 706 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq | ||||
| 707 | instantiation | 716, 717, 718, 719 | ⊢ | |
| 708 | instantiation | 751, 720, 721 | ⊢ | |
| 709 | instantiation | 751, 736, 722 | ||
| 710 | theorem | ⊢ | ||
| proveit.logic.sets.inclusion.relax_proper_subset | ||||
| 711 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.nat_pos_within_real | ||||
| 712 | instantiation | 747, 746 | ⊢ | |
| 713 | conjecture | ⊢ | ||
| proveit.numbers.exponentiation.exp_complex_closure | ||||
| 714 | instantiation | 751, 730, 723 | ⊢ | |
| 715 | instantiation | 724, 725 | ||
| 716 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real | ||||
| 717 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.zero_is_real | ||||
| 718 | instantiation | 751, 733, 726 | ⊢ | |
| 719 | axiom | ⊢ | ||
| proveit.physics.quantum.QPE._phase_in_interval | ||||
| 720 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.real_pos_within_real | ||||
| 721 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.pi_is_real_pos | ||||
| 722 | instantiation | 751, 727, 728 | ||
| 723 | instantiation | 751, 733, 729 | ⊢ | |
| 724 | conjecture | ⊢ | ||
| proveit.numbers.negation.complex_closure | ||||
| 725 | instantiation | 751, 730, 731 | ||
| 726 | instantiation | 751, 736, 746 | ⊢ | |
| 727 | instantiation | 741, 732, 743 | ||
| 728 | assumption | |||
| 729 | instantiation | 751, 736, 735 | ⊢ | |
| 730 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.complex_numbers.real_within_complex | ||||
| 731 | instantiation | 751, 733, 734 | ||
| 732 | instantiation | 744, 745, 735 | ||
| 733 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.real_numbers.rational_within_real | ||||
| 734 | instantiation | 751, 736, 737 | ||
| 735 | instantiation | 751, 749, 738 | ⊢ | |
| 736 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.rational_numbers.int_within_rational | ||||
| 737 | instantiation | 751, 739, 740 | ||
| 738 | conjecture | ⊢ | ||
| proveit.numbers.numerals.decimals.nat2 | ||||
| 739 | instantiation | 741, 742, 743 | ||
| 740 | assumption | |||
| 741 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.int_interval_within_int | ||||
| 742 | instantiation | 744, 745, 746 | ||
| 743 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.zero_is_int | ||||
| 744 | conjecture | ⊢ | ||
| proveit.numbers.addition.add_int_closure_bin | ||||
| 745 | instantiation | 747, 748 | ||
| 746 | instantiation | 751, 749, 750 | ⊢ | |
| 747 | conjecture | ⊢ | ||
| proveit.numbers.negation.int_closure | ||||
| 748 | instantiation | 751, 752, 753 | ||
| 749 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nat_within_int | ||||
| 750 | theorem | ⊢ | ||
| proveit.numbers.numerals.decimals.nat1 | ||||
| 751 | theorem | ⊢ | ||
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset | ||||
| 752 | conjecture | ⊢ | ||
| proveit.numbers.number_sets.integers.nat_pos_within_int | ||||
| 753 | assumption | |||
| *equality replacement requirements | ||||